package edu.arizona.bio5.onto.decomposition.locality;

import java.util.Collection;

import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLClassExpression;
import org.semanticweb.owlapi.model.OWLClassExpressionVisitor;
import org.semanticweb.owlapi.model.OWLDataAllValuesFrom;
import org.semanticweb.owlapi.model.OWLDataExactCardinality;
import org.semanticweb.owlapi.model.OWLDataHasValue;
import org.semanticweb.owlapi.model.OWLDataMaxCardinality;
import org.semanticweb.owlapi.model.OWLDataMinCardinality;
import org.semanticweb.owlapi.model.OWLDataSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLEntity;
import org.semanticweb.owlapi.model.OWLObjectAllValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectComplementOf;
import org.semanticweb.owlapi.model.OWLObjectExactCardinality;
import org.semanticweb.owlapi.model.OWLObjectHasSelf;
import org.semanticweb.owlapi.model.OWLObjectHasValue;
import org.semanticweb.owlapi.model.OWLObjectIntersectionOf;
import org.semanticweb.owlapi.model.OWLObjectMaxCardinality;
import org.semanticweb.owlapi.model.OWLObjectMinCardinality;
import org.semanticweb.owlapi.model.OWLObjectOneOf;
import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectUnionOf;

import com.clarkparsia.owlapi.modularity.locality.LocalityClass;

/**
 * Used to determine if class expressions are equivalent to \top using the provided locality class
 */
public class TopEquivalenceEvaluator implements OWLClassExpressionVisitor {

    private BottomEquivalenceEvaluator bottomEvaluator = new BottomEquivalenceEvaluator();

    private boolean isTopEquivalent;

    private LocalityClass localityCls;

    private Collection<? extends OWLEntity> signature;


    public TopEquivalenceEvaluator() {
    }


    private boolean isTopEquivalent(OWLClassExpression desc) {
        desc.accept(this);
        return isTopEquivalent;
    }


    public boolean isTopEquivalent(OWLClassExpression desc, Collection<? extends OWLEntity> signature, LocalityClass localityCls) {
        this.localityCls = localityCls;
        this.signature = signature;
        desc.accept(this);
        return isTopEquivalent;
    }


    public void setBottomEvaluator(BottomEquivalenceEvaluator evaluator) {
        this.bottomEvaluator = evaluator;
    }


    public void visit(OWLClass desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
                isTopEquivalent = desc.isOWLThing();
                break;
            case TOP_BOTTOM:
            case TOP_TOP:
                isTopEquivalent = desc.isOWLThing() || (!desc.isOWLNothing() && !signature.contains(desc));
                break;
        }
    }


    // BUGFIX: (TS, 2) Added the cases where the filler is top-equiv

    public void visit(OWLDataAllValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = !signature.contains(desc.getProperty().asOWLDataProperty()) || desc.getFiller().isTopDatatype();
                break;
            case TOP_TOP:
                isTopEquivalent = desc.getFiller().isTopDatatype();
                break;
        }
    }


    // BUGFIX: (TS) Added the case where this is top-equiv (including n==0).

    public void visit(OWLDataExactCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = (desc.getCardinality() == 0) && (!signature.contains(desc.getProperty().asOWLDataProperty()));
                break;
            case TOP_TOP:
                isTopEquivalent = false;
                break;
        }
    }


    // (TS) No special handling for n==0 required.

    public void visit(OWLDataMaxCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = !signature.contains(desc.getProperty().asOWLDataProperty());
                break;
            case TOP_TOP:
                isTopEquivalent = false;
                break;
        }
    }


    // BUGFIX: (TS) A data min card restriction is top-equiv iff the cardinality is 0.
    // BUGFIX: (TS, 2) Added the cases where the filler is top-equiv
    // BUGFIX: (TS, 2) Left out redundant check cardinality > 0 in TOP_TOP case
    // BUGFIX: (TS, 3) Extended the cases where the filler is top-equiv in TOP_TOP        

    public void visit(OWLDataMinCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = (desc.getCardinality() == 0);
                break;
            case TOP_TOP:
                isTopEquivalent = (desc.getCardinality() == 0) || ((desc.getCardinality() == 1) && (!signature.contains(desc.getProperty().asOWLDataProperty())) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller())) || ((desc.getCardinality() > 1) && (!signature.contains(desc.getProperty().asOWLDataProperty())) && LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller()));
                break;
        }
    }


    // BUGFIX: (TS, 2) Added the cases where the filler is top-equiv
    // BUGFIX: (TS, 3) Extended the cases where the filler is top-equiv        

    public void visit(OWLDataSomeValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = false;
                break;
            case TOP_TOP:
                isTopEquivalent = !signature.contains(desc.getProperty().asOWLDataProperty()) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller());
                break;
        }
    }


    // BUGFIX: (TS, 2) Added the cases where this is top-equiv

    public void visit(OWLDataHasValue desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = false;
                break;
            case TOP_TOP:
                isTopEquivalent = !signature.contains(desc.getProperty().asOWLDataProperty());
                break;
        }
    }


    public void visit(OWLObjectAllValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = !signature.contains(desc.getProperty().getNamedProperty()) || isTopEquivalent(desc.getFiller());
                break;
            case TOP_TOP:
                isTopEquivalent = isTopEquivalent(desc.getFiller());
                break;
        }
    }


    public void visit(OWLObjectComplementOf desc) {
        isTopEquivalent = bottomEvaluator.isBottomEquivalent(desc.getOperand(), signature, localityCls);
    }


    // BUGFIX: (TS) added the cases where this is top-equiv, including n==0

    public void visit(OWLObjectExactCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = (desc.getCardinality() == 0) && ((!signature.contains(desc.getProperty().getNamedProperty())) || bottomEvaluator.isBottomEquivalent(desc.getFiller(), signature, localityCls));
                break;
            case TOP_TOP:
                isTopEquivalent = (desc.getCardinality() == 0) && bottomEvaluator.isBottomEquivalent(desc.getFiller(), signature, localityCls);
                break;
        }
    }


    public void visit(OWLObjectIntersectionOf desc) {
        for (OWLClassExpression conj : desc.getOperands()) {
            if (!isTopEquivalent(conj)) {
                isTopEquivalent = false;
                return;
            }
        }
        isTopEquivalent = true;
    }


    // BUGFIX: (TS) Added the case of a bottom-equivalent filler to both conditions.
    //              The n==0 case doesn't affect top-equivalence of this type of restriction.

    public void visit(OWLObjectMaxCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = (!signature.contains(desc.getProperty().getNamedProperty())) || bottomEvaluator.isBottomEquivalent(desc.getFiller(), signature, localityCls);
                break;
            case TOP_TOP:
                isTopEquivalent = bottomEvaluator.isBottomEquivalent(desc.getFiller(), signature, localityCls);
                break;
        }
    }


    // BUGFIX: (TS) Added the case n==0; repaired TOP_TOP condition 
    // BUGFIX: (TS, 2) Left out redundant check cardinality > 0 in TOP_TOP case

    public void visit(OWLObjectMinCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = (desc.getCardinality() == 0);
                break;
            case TOP_TOP:
//                isTopEquivalent = !signature.contains(desc.getProperty().getNamedProperty()) && (desc.getCardinality() <= 1);
                isTopEquivalent = (desc.getCardinality() == 0) || ((!signature.contains(desc.getProperty().getNamedProperty())) && (isTopEquivalent(desc.getFiller())));
                break;
        }
    }


    public void visit(OWLObjectOneOf desc) {
        isTopEquivalent = false;
    }


    public void visit(OWLObjectHasSelf desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = false;
                break;
            case TOP_TOP:
                isTopEquivalent = !signature.contains(desc.getProperty().getNamedProperty());
                break;
        }
    }


    // BUGFIX (TS): added ".getNamedProperty()"

    public void visit(OWLObjectSomeValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = false;
                break;
            case TOP_TOP:
                isTopEquivalent = !signature.contains(desc.getProperty().getNamedProperty()) && isTopEquivalent(desc.getFiller());
                break;
        }
    }


    public void visit(OWLObjectUnionOf desc) {
        for (OWLClassExpression conj : desc.getOperands()) {
            if (isTopEquivalent(conj)) {
                isTopEquivalent = true;
                return;
            }
        }
        isTopEquivalent = false;
    }


    public void visit(OWLObjectHasValue desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isTopEquivalent = false;
                break;
            case TOP_TOP:
                isTopEquivalent = !signature.contains(desc.getProperty().getNamedProperty());
                break;
        }
    }
}
